Logic analysis and attack construction methods are two major approaches in verification of Cryptographic Protocols. However, it is almost preferable to use both of them for a complete analysis. In this paper, a generic framework for the integration of the two verification approaches is presented. Using the framework we can propose analysis methods in which security properties and breach scenarios of the properties in a protocol can be verified in a unified manner. The focus on this paper is on a computational model of the Protocols as the major component of the framework. The operational interpretation of the computational model with a term rewriting system (TRS) is presented too. To specify an intended protocol, we can represent it as a set of individual steps, and then using a transformation algorithm, a terminated and confluent TRS is generated automatically. This TRS is used to construct a special representation of the protocol named the protocol execution path, which can be used as the base of various verification schemes. Specification and verification of a sample protocol is presented too.      

This paper mirrors an invited talk to ISCISC 2011. It is not a conventional paper so much as an essay summarizing thoughts on a little-talked-about subject. My goal is to intermix some introspection about definitions with examples of them, these examples drawn mostly from cryptography. Underpinning our discussion are two themes. The first is that definitions are constructed. They are invented by man, not unearthed from the maws of scientific reality. The second theme is that definitions matter. They have been instrumental in changing the character of modern cryptography, and, I suspect, have the potential to change the character of other fields as well.

The theory of Engel groups plays an important role in group theory since these groups are closely related to the Burnside problems. In this survey we consider several classical and novel algorithmic problems for Engel groups and propose several open problems. We study these problems with a view towards applications to cryptography.

Background and Objectives: Cryptographic hash functions are the linchpins of mobile services, blockchains, and many other technologies. Designing Cryptographic hash functions has been approached by research communities from the physics, mathematics, computer science, and electrical engineering fields. The emergence of new hash functions, new hash constructions, and new requirements for application-specific hash functions, such as the ones of mobile services, have encouraged us to make a comparison of different hash functions and propose a new classification.Methods: Over 100 papers were surveyed and reviewed in detail. The research conducted in this paper has included four sections; article selection, detailed review of selected articles, data collection, and evaluation of results. Data were collected as new hash function properties, new hash function constructions, new hash function categories, and existing hash function attacks which are used to evaluate the results.Results: This paper surveys seven categories of hash functions including block cipher-based functions, algebraic-based functions, custom-designed functions, Memory-hard Functions (MHFs), Physical Unclonable Functions (PUFs), quantum hash functions and optical hash functions. To the best of our knowledge, the last four mentioned categories have not been sufficiently addressed in most existing surveys. Furthermore, this paper overviews hash-related adversaries and six hash construction variants. In addition, we employed the mentioned adversaries as evaluation criteria to illustrate how different categories of hash functions withstand the mentioned adversaries. Finally, the surveyed hash function categories were evaluated against mobile service requirements.Conclusion: In addition to new classification, our findings suggest using PUFs with polynomial-time error correction or possibly bitwise equivalents of algebraic structures that belongs to post-quantum cryptography as candidates to assist mobile service interaction requirements.